The present invention relates generally to the field of circuit design. More specifically, the invention relates to the design of integrated circuits which may be modified or optimized during a design process.
For the design of digital circuits on the scale of VLSI (Very Large Scale Integration) technology, designers often employ computer-aided techniques. Standard languages such as hardware description languages (HDLs) have been developed to describe digital circuits to aid in the design and simulation of complex digital circuits. Several hardware description languages, such as VHDL and Verilog, have evolved as industry standards. VHDL and Verilog are general-purpose hardware description languages that allow definition of a hardware model at the gate level, the register transfer level (RTL), or the behavioral level using abstract data types. As device technology and design technology continues to advance, various product design tools have been developed to adapt HDLs for use with newer devices and design styles and to also allow for the optimization of a design after the compilation of an HDL code which describes a particular circuit.
FIG. 1 illustrates an example in the prior art in which a circuit is initially designed and then optimized in the design process. The optimized design typically must be compared with the original design to verify that the optimized design is equivalent to the initial or original design. This is often required because the optimization process may result in a change to the design which causes the second design (e.g. an optimized design) to not be an equivalent circuit such that the optimized design does not produce the same result for a given input as the initial design.
The process of FIG. 1 starts at block 100. At block 110, an HDL code is prepared for a particular circuit. This code is typically compiled in an HDL compiler to generate a first RTL netlist, as shown in block 120. Then at block 140, the first RTL netlist is processed in order to optimize the design which results in a technology map. The optimization process may include, for example, redundancy removal, state machine re-encoding, flip-flop replication, retiming, pipelining, half-cycle scheduling, and conversions between clock gating and enables.
At block 160, a verification tool, such as a commercially available verification software product, is used to check for equivalence between the first RTL netlist and the technology map. At block 170, the use of this tool results in a test to determine whether the two netlists are equivalent. If these two netlists are not equivalent, this results in an error message being displayed to the designer by the verification tool, as shown in 180. On the other hand, if the verification tool can verify that the two netlists are equivalent, then an indication of this equivalence is displayed to the designer and the process may proceed to block 190 in which place and route tools are used to create an integrated circuit from the technology map. The process stops at block 200.
Typically in the prior art, the equivalence checking of the first RTL representation and the mapped representation performed in block 160 requires an exhaustive simulation of the circuits by going through all possible input vectors. FIG. 2A illustrates an example of a circuit used to test for non-equivalence. The circuit 200 includes five (5) inputs 210-214 and one output 215. FIG. 2B is a truth table illustrating the 32 input vectors for the circuit 200. Equivalence checking tools that are commercially available include Formality from Synopsis, Mountain View, Calif., Crysalys from Avant!, Fremont, Calif., Formal Pro from Mentor Graphics, Wilsonville, Oreg., Conformal from Verplex, Milpitas, Calif., etc. When the circuit has a large number of input vectors, the testing of the circuit using all of the input vectors can require a lot of memory and be very time consuming.
According to one aspect of the present invention, an exemplary method for determining non-equivalence between two netlists is disclosed. Matched registers between the two netlists are determined. The matched registers become cut off points to generate primary inputs and outputs. When there are one or more unmatched registers between the first netlist and the second netlist, the unmatched registers are pushed to the primary inputs or outputs using retiming. The primary inputs of the resulting circuits after using retiming are then driven by a function of subspace variables. The circuits are then verified with all possible values of the subspace variable.
The present invention also discloses apparatuses, including software media which may be used to design integrated circuits. For example, the present invention includes digital processing systems which are capable of designing integrated circuits according to the present invention, and the invention also includes machine readable media, which when executed on a digital processing system such as a computer system, causes the digital processing system to execute a method for designing integrated circuits.